FDL - Step of Proof: p-co-restrict

Step of Proof: p-co-restrict_wf

11,40

Inference at *
Iof proof for Lemma p-co-restrict wf:

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))).

p-co-restrict(f;p)

(B + Top)

by ((Unfold `p-co-restrict` 0)
CollapseTHEN (Auto

))

Co.

Definitions p-co-restrict(f;p), f o g , p-co-filter(f), x. t(x), x.A(x), Dec(P), x:A. B(x), x(s), f(a), , x:AB(x), left + right, Top, t T, Type

Lemmas p-compose wf, p-co-filter wf, decidable wf, top wf

Definitions	p-co-restrict(f;p), f o g , p-co-filter(f), x. t(x), x.A(x), Dec(P), x:A. B(x), x(s), f(a), , x:AB(x), left + right, Top, t T, Type
Lemmas	p-compose wf, p-co-filter wf, decidable wf, top wf